only k(v):B sends [tg,f(s;v)] : T on l
== (e:E.
== ((loc(e) = source(l))  (kind(e) = k)  (e':E. ((kind(e') = rcv(l,tg)) c (sender(e') = e))))
== & (e':E.
== & ((kind(e') = rcv(l,tg))
== & ( ((kind(sender(e')) = k)
== & ( c (valtype(sender(e')) r B)
== & ( c (valtype(e') r T)
== & ( c (val(e') = f((state when sender(e'));val(sender(e')))
== & ( c & (e'':E. (kind(e'') = rcv(l,tg))  (sender(e'') = sender(e'))  (e'' = e'))))) 

latex

---

clarification:

es-only-sender(es; k; B; l; tg; T; s,v.f(s;v))
== (e:es-E(es).
== ((es-loc(es; e) = source(l)  Id)
== ( (es-kind(es; e) = k  Knd)
== ( (e':es-E(es). ((es-kind(es; e') = rcv(l,tg)  Knd) c (es-sender(es; e') = e  es-E(es)))))
== & (e':es-E(es).
== & ((es-kind(es; e') = rcv(l,tg)  Knd)
== & ( ((es-kind(es; es-sender(es; e')) = k  Knd)
== & ( c (es-valtype(es; es-sender(es; e')) r B)
== & ( c (es-valtype(es; e') r T)
== & ( c (es-val(es; e')
== & ( c (=
== & ( c (f(es-state-when(es;es-sender(es; e'));es-val(es; es-sender(es; e')))
== & ( c ( T
== & ( c & (e'':es-E(es).
== & ( c & ((es-kind(es; e'') = rcv(l,tg)  Knd)
== & ( c & ( (es-sender(es; e'') = es-sender(es; e')  es-E(es))
== & ( c & ( (e'' = e'  es-E(es)))))) 

latex

Definitions	Id, loc(e), source(l), x:A. B(x), A c B, valtype(e), P & Q, (state when e), val(e), x:A. B(x), Knd, kind(e), rcv(l,tg), P  Q, sender(e), E
FDL editor aliases	es-only-sender